Inference at * 
Iof proof for Lemma adjacent-append:


  T:Type, x, y:T, L1, L2:(T List).
  adjacent(T;L1 @ L2;x;y)
   (adjacent(T;L1;x;y)
    ((0 < ||L1||) & (0 < ||L2||) & x = last(L1) & y = hd(L2))
    adjacent(T;L2;x;y)) 

latex

 by ((RepUR``adjacent`` 0) 
CollapseTHEN (((MaAuto) 
CollapseTHEN (((ExRepD) 
CollapseTHEN (
CAuto')))))) 

latex

C1: 

C1: 1. T : Type
C1: 2. x : T
C1: 3. y : T
C1: 4. L1 : T List
C1: 5. L2 : T List
C1: 6. i : {0..(||L1 @ L2|| - 1)}
C1: 7. x = (L1 @ L2)[i]
C1: 8. y = (L1 @ L2)[(i+1)]
C1:   (i:{0..(||L1|| - 1)}. (x = L1[i] & y = L1[(i+1)]))
C1:    ((0 < ||L1||) & (0 < ||L2||) & x = last(L1) & y = hd(L2))
C1:    (i:{0..(||L2|| - 1)}. (x = L2[i] & y = L2[(i+1)]))
C2: 

C2: 1. T : Type
C2: 2. x : T
C2: 3. y : T
C2: 4. L1 : T List
C2: 5. L2 : T List
C2: 6. (i:{0..(||L1|| - 1)}. (x = L1[i] & y = L1[(i+1)]))
C2: 6.  ((0 < ||L1||) & (0 < ||L2||) & x = last(L1) & y = hd(L2))
C2: 6.  (i:{0..(||L2|| - 1)}. (x = L2[i] & y = L2[(i+1)]))
C2:   i:{0..(||L1 @ L2|| - 1)}. (x = (L1 @ L2)[i] & y = (L1 @ L2)[(i+1)])
C3: 

C3: 1. T : Type
C3: 2. T
C3: 3. T
C3: 4. L1 : T List
C3: 5. L2 : T List
C3: 6. 0 < ||L1||
C3: 7. 0 < ||L2||
C3:   (null(L1))
C.

Definitions

adjacent(T;L;x;y), (x  l), x. t(x), x:A.B(x), (xL.P(x)), xL. P(x), |r|, x f y, f(a), a < b, |g|, a <p b, a  b, |p|, a ~ b, b | a, x,y:A//B(x;y), Atom, P  Q, Dec(P), as @ bs, P  Q, i  j < k, n - m, -n, n+m, , l[i], A  B, A c B, Void, False, , #$n, <a, b>, last(L), hd(l), x:A. B(x), P  Q, x:AB(x), t  T, {x:A| B(x)} , , P  Q, left + right, x:A. B(x), P & Q, x:A  B(x), s = t, {i..j}, a < b, type List, Type, A, b, ||as||, i  j

Lemmas

iff wf, decidable or, decidable lt, decidable ex int seg, decidable cand, append wf, rev implies wf, length wf1, select wf, last wf, false wf, hd wf, int seg wf, assert wf, not wf